Nuprl Lemma : opt_wf
4,23
postcript
pdf
T
:Type,
x
:
T
,
b
:
. (
b
?
x
)
T
+Unit
latex
Definitions
(
b
?
x
)
,
if
b
t
else
f
fi
,
x
:
A
.
B
(
x
)
,
Unit
,
,
,
t
T
Lemmas
bool
wf
,
it
wf
,
unit
wf
,
ifthenelse
wf
origin
T:Type, x:T, b:
. (b?x) 
T+Unit T:Type, x:T, b:. (b?x) T+Unit 
t else f fix:A. B(x)
T